『Lean4Lean: Verifying a Typechecker for Lean, in Lean』
1. どんなもの？
2. 先行研究と比べてどこがすごい？
3. 技術や手法のキモはどこ？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
MetaRocq に関する論文（Sozeau et al., 2019/2020）, Rocq の形式検証フレームワーク。 Sozeau et al. (2020)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2020. The MetaCoq Project. Journal of Automated Reasoning (Feb. 2020). https://doi.org/10.1007/s10817-019-09540-0 Sozeau et al. (2019)
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2019. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. 4, POPL, Article 8 (dec 2019), 28 pages. https://doi.org/10.1145/3371076 de Moura et al. (2015). The Lean Theorem Prover (system description), Leanの基本設計。
証明支援系の自己検証に関する古典的研究（例: HOL Light, Isabelle の自己検証論文）。
メモ
確認用
Q.